Nuprl Lemma : compat-iseg
11,40
postcript
pdf
T
:Type,
L1
,
L2
,
L3
:(
T
List). iseg(
T
;
L1
;
L2
)
compat(
T
;
L2
;
L3
)
compat(
T
;
L1
;
L3
)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
compat(
T
;
l1
;
l2
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
append(
as
;
bs
)
,
prop{i:l}
,
iseg(
T
;
l1
;
l2
)
Lemmas
append
wf
,
compat-append
,
append
nil
sq
,
compat
wf
origin
T:Type, L1,L2,L3:(T List). iseg(T; L1; L2) 
compat(T; L2; L3) compat(T; L1; L3) T:Type, L1,L2,L3:(T List). iseg(T; L1; L2) compat(T; L2; L3) compat(T; L1; L3) 
Tx:A. B(x) Q
x:A. B(x)